Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar14/curryingSLASHAG01SLASHHASH3.57.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(minus, x), y)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y))
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(plus, x)
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(app'₂(plus, x), y)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(quot, app'₂(app'₂(minus, x), y))
APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))
APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(app'₂(plus, x), y)
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(s, app'₂(app'₂(plus, x), y))
APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k))))
APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(plus, x)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(minus, x)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(app'₂(plus, y), z)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(plus, y)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l)
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(cons, app'₂(app'₂(plus, x), y))
APP'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> APP'₂(minus, x)
APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))
APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app, l)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(minus, x), y)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app'₂(app, l), k)

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(minus, x), y)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y))
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(plus, x)
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(app'₂(plus, x), y)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(quot, app'₂(app'₂(minus, x), y))
APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))
APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(app'₂(plus, x), y)
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(s, app'₂(app'₂(plus, x), y))
APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k))))
APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(plus, x)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(minus, x)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(app'₂(plus, y), z)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(plus, y)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l)
APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(cons, app'₂(app'₂(plus, x), y))
APP'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> APP'₂(minus, x)
APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))
APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app, l)
APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(minus, x), y)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app'₂(app, l), k)

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 6 SCCs with 17 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app'₂(app, l), k)

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

APP'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> APP'₂(app'₂(app, l), k)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
APP'₂(x1, x2) = APP'₁(x1)
app'₂(x1, x2) = app'₁(x2)
app = app
cons = cons

Lexicographic Path Order [19].
Precedence:

APP'₁ > [app'₁, app, cons]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(app'₂(plus, x), y)

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

APP'₂(app'₂(plus, app'₂(s, x)), y) -> APP'₂(app'₂(plus, x), y)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
APP'₂(x1, x2) = x1
app'₂(x1, x2) = app'₁(x2)
plus = plus
s = s

Lexicographic Path Order [19].
Precedence:

[plus, s]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

APP'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> APP'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
APP'₂(x1, x2) = APP'₁(x2)
sum = sum
app'₂(x1, x2) = app'₁(x2)
cons = cons
plus = plus
0 = 0
s = s

Lexicographic Path Order [19].
Precedence:

[APP'₁, cons] > sum > app'₁ > plus
0 > plus
s > plus

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> APP'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(minus, x), y)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

APP'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(minus, x), y)
APP'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> APP'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
APP'₂(x1, x2) = APP'₁(x1)
app'₂(x1, x2) = app'₂(x1, x2)
minus = minus
s = s
plus = plus
0 = 0

Lexicographic Path Order [19].
Precedence:

APP'₁ > [app'₂, s] > plus
minus > [app'₂, s] > plus

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> APP'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y))

The TRS R consists of the following rules:

app'₂(app'₂(minus, x), 0) -> x
app'₂(app'₂(minus, app'₂(s, x)), app'₂(s, y)) -> app'₂(app'₂(minus, x), y)
app'₂(app'₂(minus, app'₂(app'₂(minus, x), y)), z) -> app'₂(app'₂(minus, x), app'₂(app'₂(plus, y), z))
app'₂(app'₂(quot, 0), app'₂(s, y)) -> 0
app'₂(app'₂(quot, app'₂(s, x)), app'₂(s, y)) -> app'₂(s, app'₂(app'₂(quot, app'₂(app'₂(minus, x), y)), app'₂(s, y)))
app'₂(app'₂(plus, 0), y) -> y
app'₂(app'₂(plus, app'₂(s, x)), y) -> app'₂(s, app'₂(app'₂(plus, x), y))
app'₂(app'₂(app, nil), k) -> k
app'₂(app'₂(app, l), nil) -> l
app'₂(app'₂(app, app'₂(app'₂(cons, x), l)), k) -> app'₂(app'₂(cons, x), app'₂(app'₂(app, l), k))
app'₂(sum, app'₂(app'₂(cons, x), nil)) -> app'₂(app'₂(cons, x), nil)
app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), l))) -> app'₂(sum, app'₂(app'₂(cons, app'₂(app'₂(plus, x), y)), l))
app'₂(sum, app'₂(app'₂(app, l), app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))) -> app'₂(sum, app'₂(app'₂(app, l), app'₂(sum, app'₂(app'₂(cons, x), app'₂(app'₂(cons, y), k)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.